\section{Компилятор из L в код\\
для стековой машины}

Метки: $L=\term{Yes}\;\NN\mid\term{Maybe}\;\NN\mid\term{No}$.

Дополнительное преобразование $\term{Force} : L\to L$:

$$
\begin{array}{rcl}
  \term{Force}\;(\term{Maybe}\;n)&=&\term{Yes}\;n\\
  \term{Force}\;(\term{Yes}\;n)&=&\term{Yes}\;n
\end{array}
$$

Два преобразования программ $\cal P$ для стековой машины:

$$
\term{First},\;\term{Last} : L \to{\cal P}\to{\cal P}
$$

$$
\begin{array}{rcl}
  \term{First}\;(\term{Yes}\;n,\;IP)&=&\{\$n:I\}P\\
  \term{First}\;(\term{No},\;P)&=&P\\
  \term{Last}\;(\term{Yes}\;n,\;P)&=&P\{\cd{J }\$n\}\\
  \term{Last}\;(\term{Maybe}\;\_,\;P)&=&P
\end{array}
$$

Обрамление: 

$$
\term{Frame}:L\times L\to{\cal P}\to{\cal P}
$$

$$
\term{Frame}\;(f, l, P)=\term{Last}\;(l,\;\term{First}\;(f,\;P))
$$

\begin{itemize}
\item Компилятор выражений: 


$$
\withenv{this}{\trans{x}{}{\term{First}\;(this,\;\term{L}x)}}
$$

$$
\withenv{this}{\trans{z}{}{\term{First}\;(this,\;\term{C}z)}}
$$

$$
\trule{\withenv{this}{\trans{A}{}{A^\prime}},\;\withenv{\term{No}}{\trans{B}{}{B^\prime}}}
      {\withenv{this}{\trans{A\otimes B}{}{A^\prime B^\prime\{\term{B}\otimes}\}}}
$$

\item Компилятор операторов:

$$
\trule{\withenv{this}{\trans{e}{}{e^\prime}}}
      {\withenv{\inbr{this,next,last}}{\trans{\llang{$x$:=$e$}}{}{\inbr{\term{Last}\;(next,\;e^\prime\{\term{S}x\}),\;last}}}}
$$

$$
\trule{\withenv{this}{\trans{e}{}{e^\prime}}}
      {\withenv{\inbr{this,next,last}}{\trans{\llang{write$\;e$}}{}{\inbr{\term{Last}\;(next,\;e^\prime\term{W}),\;last}}}}
$$

$$
\withenv{\inbr{this,next,last}}{\trans{\llang{read$\;x$}}{}{\inbr{\term{Frame}\;(this,next,\term{R}\{\term{S}x\}),\;last}}}
$$

$$
\trule{
   \begin{array}{c}       
     \withenv{this}{\trans{e}{}{e^\prime}}\\
     \withenv{\inbr{\term{No},\term{Force}\;(next), last+1}}{\trans{S_2}{}{\inbr{S_2^\prime,last^\prime}}}\\
     \withenv{\inbr{\term{Yes}\;(last+1),next,last^\prime}}{\trans{S_1}{}{\inbr{S_1^\prime,last^{\prime\prime}}}}
   \end{array}
}
{\withenv{\inbr{this,next,last}}{\trans{\llang{if$\;e\;$then$\;S_1\;$else$\;S_2\;$}}{}{\inbr{e^\prime\{\term{JT}\$(last+1)\}S_2^\prime S_1^\prime, last^{\prime\prime}}}}}
$$

$$
\trule{
   \begin{array}{c}
       \withenv{\term{Yes}\;(last+1)}{\trans{e}{}{e^\prime}}\\
       \withenv{\inbr{\term{Yes}\;(last+2),\term{Maybe}\;(last+1),last+2}}{\trans{S}{}{\inbr{S^\prime,last^\prime}}}
   \end{array}
      }
      {\withenv{\inbr{this,next,last}}{\trans{\llang{while$\;e\;$do$\;S\;$}}{}{\inbr{\term{Frame}\;(this,next,\{\term{J}\$(last+1)\}S^\prime e^\prime\{\term{JT}\$(last+2)\}),last^\prime}}}}
$$

$$
\trule{
   \begin{array}{c}
       \withenv{\inbr{this,\term{Maybe}\;(last+1), last+1}}{\trans{S_1}{}{\inbr{S_1^\prime,last^\prime}}}\\
       \withenv{\inbr{\term{Yes}\;(last+1),next,last^\prime}}{\trans{S_2}{}{\inbr{S_2^\prime,last^{\prime\prime}}}}
   \end{array}
      }
      {\withenv{\inbr{this,next,last}}{\trans{\llang{$S_1\;$;$\;S_2$}}{}{\inbr{S_1^\prime S_2^\prime,last^{\prime\prime}}}}}
$$

$$
\withenv{\inbr{\term{No},\term{Maybe}\;n,last}}{\trans{\llang{skip}}{}{\inbr{\epsilon,last}}}
$$

$$
\withenv{\inbr{\term{No},\term{Yes}\;n,last}}{\trans{\llang{skip}}{}{\inbr{\{\term{J}\$n\},last}}}
$$

$$
\withenv{\inbr{\term{Yes}\;m,\term{Maybe}\;n,last}}{\trans{\llang{skip}}{}{\inbr{\$m:\{\term{J}\$n\},last}}}
$$

$$
\withenv{\inbr{\term{Yes}\;m,\term{Yes}\;n,last}}{\trans{\llang{skip}}{}{\inbr{\$m:\{\term{J}\$n\},last}}}
$$

\end{itemize}

Компилятор для всей программы:

$$
\sembr{P}=C\{0\term{E}\},\mbox{ где } \withenv{\inbr{\term{No}, \term{Maybe}\;0, 0}}{\trans{P}{}{\inbr{C,\_}}}
$$
